YES 1.252
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ BR
mainModule Main
| ((notElem :: Eq a => a -> [a] -> Bool) :: Eq a => a -> [a] -> Bool) |
module Main where
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
| ((notElem :: Eq a => a -> [a] -> Bool) :: Eq a => a -> [a] -> Bool) |
module Main where
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
mainModule Main
| (notElem :: Eq a => a -> [a] -> Bool) |
module Main where
Haskell To QDPs
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(xv1400), Succ(xv401000)) → new_primPlusNat(xv1400, xv401000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(xv1400), Succ(xv401000)) → new_primPlusNat(xv1400, xv401000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(xv3100), Succ(xv40100)) → new_primMulNat(xv3100, Succ(xv40100))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(xv3100), Succ(xv40100)) → new_primMulNat(xv3100, Succ(xv40100))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(xv300), Succ(xv4000)) → new_primEqNat(xv300, xv4000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(xv300), Succ(xv4000)) → new_primEqNat(xv300, xv4000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, dg, app(app(ty_@2, eg), eh)) → new_esEs3(xv32, xv402, eg, eh)
new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), app(app(ty_Either, gd), ge), dg, fc) → new_esEs(xv30, xv400, gd, ge)
new_esEs3(@2(xv30, xv31), @2(xv400, xv401), bbh, app(ty_Maybe, bcg)) → new_esEs2(xv31, xv401, bcg)
new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), app(ty_[], ha), dg, fc) → new_esEs1(xv30, xv400, ha)
new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), app(ty_Maybe, hb), dg, fc) → new_esEs2(xv30, xv400, hb)
new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, dg, app(ty_Maybe, ef)) → new_esEs2(xv32, xv402, ef)
new_esEs2(Just(xv30), Just(xv400), app(app(ty_Either, bag), bah)) → new_esEs(xv30, xv400, bag, bah)
new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, app(ty_[], fh), fc) → new_esEs1(xv31, xv401, fh)
new_esEs(Right(xv30), Right(xv400), cc, app(app(app(ty_@3, cf), cg), da)) → new_esEs0(xv30, xv400, cf, cg, da)
new_esEs(Right(xv30), Right(xv400), cc, app(ty_[], db)) → new_esEs1(xv30, xv400, db)
new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, dg, app(app(ty_Either, dh), ea)) → new_esEs(xv32, xv402, dh, ea)
new_esEs1(:(xv30, xv31), :(xv400, xv401), he) → new_esEs1(xv31, xv401, he)
new_esEs(Right(xv30), Right(xv400), cc, app(app(ty_@2, dd), de)) → new_esEs3(xv30, xv400, dd, de)
new_esEs3(@2(xv30, xv31), @2(xv400, xv401), app(app(app(ty_@3, bde), bdf), bdg), bdd) → new_esEs0(xv30, xv400, bde, bdf, bdg)
new_esEs1(:(xv30, xv31), :(xv400, xv401), app(ty_[], bac)) → new_esEs1(xv30, xv400, bac)
new_esEs3(@2(xv30, xv31), @2(xv400, xv401), bbh, app(ty_[], bcf)) → new_esEs1(xv31, xv401, bcf)
new_esEs2(Just(xv30), Just(xv400), app(ty_[], bbd)) → new_esEs1(xv30, xv400, bbd)
new_esEs2(Just(xv30), Just(xv400), app(ty_Maybe, bbe)) → new_esEs2(xv30, xv400, bbe)
new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, app(app(app(ty_@3, fd), ff), fg), fc) → new_esEs0(xv31, xv401, fd, ff, fg)
new_esEs(Left(xv30), Left(xv400), app(app(app(ty_@3, bd), be), bf), bc) → new_esEs0(xv30, xv400, bd, be, bf)
new_esEs3(@2(xv30, xv31), @2(xv400, xv401), app(ty_[], bdh), bdd) → new_esEs1(xv30, xv400, bdh)
new_esEs(Left(xv30), Left(xv400), app(ty_Maybe, bh), bc) → new_esEs2(xv30, xv400, bh)
new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, app(app(ty_@2, gb), gc), fc) → new_esEs3(xv31, xv401, gb, gc)
new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, dg, app(ty_[], ee)) → new_esEs1(xv32, xv402, ee)
new_esEs2(Just(xv30), Just(xv400), app(app(app(ty_@3, bba), bbb), bbc)) → new_esEs0(xv30, xv400, bba, bbb, bbc)
new_esEs3(@2(xv30, xv31), @2(xv400, xv401), bbh, app(app(ty_@2, bch), bda)) → new_esEs3(xv31, xv401, bch, bda)
new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), app(app(ty_@2, hc), hd), dg, fc) → new_esEs3(xv30, xv400, hc, hd)
new_esEs1(:(xv30, xv31), :(xv400, xv401), app(app(ty_@2, bae), baf)) → new_esEs3(xv30, xv400, bae, baf)
new_esEs(Right(xv30), Right(xv400), cc, app(app(ty_Either, cd), ce)) → new_esEs(xv30, xv400, cd, ce)
new_esEs(Left(xv30), Left(xv400), app(app(ty_@2, ca), cb), bc) → new_esEs3(xv30, xv400, ca, cb)
new_esEs3(@2(xv30, xv31), @2(xv400, xv401), app(ty_Maybe, bea), bdd) → new_esEs2(xv30, xv400, bea)
new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, dg, app(app(app(ty_@3, eb), ec), ed)) → new_esEs0(xv32, xv402, eb, ec, ed)
new_esEs1(:(xv30, xv31), :(xv400, xv401), app(ty_Maybe, bad)) → new_esEs2(xv30, xv400, bad)
new_esEs3(@2(xv30, xv31), @2(xv400, xv401), app(app(ty_@2, beb), bec), bdd) → new_esEs3(xv30, xv400, beb, bec)
new_esEs(Right(xv30), Right(xv400), cc, app(ty_Maybe, dc)) → new_esEs2(xv30, xv400, dc)
new_esEs1(:(xv30, xv31), :(xv400, xv401), app(app(app(ty_@3, hh), baa), bab)) → new_esEs0(xv30, xv400, hh, baa, bab)
new_esEs3(@2(xv30, xv31), @2(xv400, xv401), bbh, app(app(ty_Either, bca), bcb)) → new_esEs(xv31, xv401, bca, bcb)
new_esEs2(Just(xv30), Just(xv400), app(app(ty_@2, bbf), bbg)) → new_esEs3(xv30, xv400, bbf, bbg)
new_esEs3(@2(xv30, xv31), @2(xv400, xv401), app(app(ty_Either, bdb), bdc), bdd) → new_esEs(xv30, xv400, bdb, bdc)
new_esEs(Left(xv30), Left(xv400), app(ty_[], bg), bc) → new_esEs1(xv30, xv400, bg)
new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, app(app(ty_Either, fa), fb), fc) → new_esEs(xv31, xv401, fa, fb)
new_esEs3(@2(xv30, xv31), @2(xv400, xv401), bbh, app(app(app(ty_@3, bcc), bcd), bce)) → new_esEs0(xv31, xv401, bcc, bcd, bce)
new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, app(ty_Maybe, ga), fc) → new_esEs2(xv31, xv401, ga)
new_esEs1(:(xv30, xv31), :(xv400, xv401), app(app(ty_Either, hf), hg)) → new_esEs(xv30, xv400, hf, hg)
new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), app(app(app(ty_@3, gf), gg), gh), dg, fc) → new_esEs0(xv30, xv400, gf, gg, gh)
new_esEs(Left(xv30), Left(xv400), app(app(ty_Either, ba), bb), bc) → new_esEs(xv30, xv400, ba, bb)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_esEs2(Just(xv30), Just(xv400), app(app(app(ty_@3, bba), bbb), bbc)) → new_esEs0(xv30, xv400, bba, bbb, bbc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Just(xv30), Just(xv400), app(app(ty_@2, bbf), bbg)) → new_esEs3(xv30, xv400, bbf, bbg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(:(xv30, xv31), :(xv400, xv401), app(app(app(ty_@3, hh), baa), bab)) → new_esEs0(xv30, xv400, hh, baa, bab)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(:(xv30, xv31), :(xv400, xv401), app(app(ty_@2, bae), baf)) → new_esEs3(xv30, xv400, bae, baf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Just(xv30), Just(xv400), app(ty_Maybe, bbe)) → new_esEs2(xv30, xv400, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(:(xv30, xv31), :(xv400, xv401), app(ty_Maybe, bad)) → new_esEs2(xv30, xv400, bad)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Just(xv30), Just(xv400), app(app(ty_Either, bag), bah)) → new_esEs(xv30, xv400, bag, bah)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Just(xv30), Just(xv400), app(ty_[], bbd)) → new_esEs1(xv30, xv400, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(:(xv30, xv31), :(xv400, xv401), app(app(ty_Either, hf), hg)) → new_esEs(xv30, xv400, hf, hg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@2(xv30, xv31), @2(xv400, xv401), app(app(app(ty_@3, bde), bdf), bdg), bdd) → new_esEs0(xv30, xv400, bde, bdf, bdg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(@2(xv30, xv31), @2(xv400, xv401), bbh, app(app(app(ty_@3, bcc), bcd), bce)) → new_esEs0(xv31, xv401, bcc, bcd, bce)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs3(@2(xv30, xv31), @2(xv400, xv401), bbh, app(app(ty_@2, bch), bda)) → new_esEs3(xv31, xv401, bch, bda)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@2(xv30, xv31), @2(xv400, xv401), app(app(ty_@2, beb), bec), bdd) → new_esEs3(xv30, xv400, beb, bec)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@2(xv30, xv31), @2(xv400, xv401), bbh, app(ty_Maybe, bcg)) → new_esEs2(xv31, xv401, bcg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@2(xv30, xv31), @2(xv400, xv401), app(ty_Maybe, bea), bdd) → new_esEs2(xv30, xv400, bea)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@2(xv30, xv31), @2(xv400, xv401), bbh, app(app(ty_Either, bca), bcb)) → new_esEs(xv31, xv401, bca, bcb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@2(xv30, xv31), @2(xv400, xv401), app(app(ty_Either, bdb), bdc), bdd) → new_esEs(xv30, xv400, bdb, bdc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@2(xv30, xv31), @2(xv400, xv401), bbh, app(ty_[], bcf)) → new_esEs1(xv31, xv401, bcf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@2(xv30, xv31), @2(xv400, xv401), app(ty_[], bdh), bdd) → new_esEs1(xv30, xv400, bdh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(Right(xv30), Right(xv400), cc, app(app(app(ty_@3, cf), cg), da)) → new_esEs0(xv30, xv400, cf, cg, da)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs(Left(xv30), Left(xv400), app(app(app(ty_@3, bd), be), bf), bc) → new_esEs0(xv30, xv400, bd, be, bf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, app(app(app(ty_@3, fd), ff), fg), fc) → new_esEs0(xv31, xv401, fd, ff, fg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, dg, app(app(app(ty_@3, eb), ec), ed)) → new_esEs0(xv32, xv402, eb, ec, ed)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), app(app(app(ty_@3, gf), gg), gh), dg, fc) → new_esEs0(xv30, xv400, gf, gg, gh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(Right(xv30), Right(xv400), cc, app(app(ty_@2, dd), de)) → new_esEs3(xv30, xv400, dd, de)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(Left(xv30), Left(xv400), app(app(ty_@2, ca), cb), bc) → new_esEs3(xv30, xv400, ca, cb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, dg, app(app(ty_@2, eg), eh)) → new_esEs3(xv32, xv402, eg, eh)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, app(app(ty_@2, gb), gc), fc) → new_esEs3(xv31, xv401, gb, gc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), app(app(ty_@2, hc), hd), dg, fc) → new_esEs3(xv30, xv400, hc, hd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(Left(xv30), Left(xv400), app(ty_Maybe, bh), bc) → new_esEs2(xv30, xv400, bh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(Right(xv30), Right(xv400), cc, app(ty_Maybe, dc)) → new_esEs2(xv30, xv400, dc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(Right(xv30), Right(xv400), cc, app(app(ty_Either, cd), ce)) → new_esEs(xv30, xv400, cd, ce)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(Left(xv30), Left(xv400), app(app(ty_Either, ba), bb), bc) → new_esEs(xv30, xv400, ba, bb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(Right(xv30), Right(xv400), cc, app(ty_[], db)) → new_esEs1(xv30, xv400, db)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(Left(xv30), Left(xv400), app(ty_[], bg), bc) → new_esEs1(xv30, xv400, bg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(:(xv30, xv31), :(xv400, xv401), he) → new_esEs1(xv31, xv401, he)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_esEs1(:(xv30, xv31), :(xv400, xv401), app(ty_[], bac)) → new_esEs1(xv30, xv400, bac)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, dg, app(ty_Maybe, ef)) → new_esEs2(xv32, xv402, ef)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), app(ty_Maybe, hb), dg, fc) → new_esEs2(xv30, xv400, hb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, app(ty_Maybe, ga), fc) → new_esEs2(xv31, xv401, ga)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), app(app(ty_Either, gd), ge), dg, fc) → new_esEs(xv30, xv400, gd, ge)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, dg, app(app(ty_Either, dh), ea)) → new_esEs(xv32, xv402, dh, ea)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, app(app(ty_Either, fa), fb), fc) → new_esEs(xv31, xv401, fa, fb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), app(ty_[], ha), dg, fc) → new_esEs1(xv30, xv400, ha)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, app(ty_[], fh), fc) → new_esEs1(xv31, xv401, fh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs0(@3(xv30, xv31, xv32), @3(xv400, xv401, xv402), df, dg, app(ty_[], ee)) → new_esEs1(xv32, xv402, ee)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_foldr(xv3, :(xv40, xv41), ba) → new_foldr(xv3, xv41, ba)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldr(xv3, :(xv40, xv41), ba) → new_foldr(xv3, xv41, ba)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3